| 1: | g(A) | → A | |
| 2: | g(B) | → A | |
| 3: | g(B) | → B | |
| 4: | g(C) | → A | |
| 5: | g(C) | → B | |
| 6: | g(C) | → C | |
| 7: | foldB(t,0) | → t | |
| 8: | foldB(t,s(n)) | → f(foldB(t,n),B) | |
| 9: | foldC(t,0) | → t | |
| 10: | foldC(t,s(n)) | → f(foldC(t,n),C) | |
| 11: | f(t,x) | → f'(t,g(x)) | |
| 12: | f'(triple(a,b,c),C) | → triple(a,b,s(c)) | |
| 13: | f'(triple(a,b,c),B) | → f(triple(a,b,c),A) | |
| 14: | f'(triple(a,b,c),A) | → f''(foldB(triple(s(a),0,c),b)) | |
| 15: | f''(triple(a,b,c)) | → foldC(triple(a,b,0),c) | |
| 16: | fold(t,x,0) | → t | |
| 17: | fold(t,x,s(n)) | → f(fold(t,x,n),x) | |
| 18: | FOLDB(t,s(n)) | → F(foldB(t,n),B) | |
| 19: | FOLDB(t,s(n)) | → FOLDB(t,n) | |
| 20: | FOLDC(t,s(n)) | → F(foldC(t,n),C) | |
| 21: | FOLDC(t,s(n)) | → FOLDC(t,n) | |
| 22: | F(t,x) | → F'(t,g(x)) | |
| 23: | F(t,x) | → G(x) | |
| 24: | F'(triple(a,b,c),B) | → F(triple(a,b,c),A) | |
| 25: | F'(triple(a,b,c),A) | → F''(foldB(triple(s(a),0,c),b)) | |
| 26: | F'(triple(a,b,c),A) | → FOLDB(triple(s(a),0,c),b) | |
| 27: | F''(triple(a,b,c)) | → FOLDC(triple(a,b,0),c) | |
| 28: | FOLD(t,x,s(n)) | → F(fold(t,x,n),x) | |
| 29: | FOLD(t,x,s(n)) | → FOLD(t,x,n) | |